Skip to content

Conversation

@tmke8
Copy link
Owner

@tmke8 tmke8 commented Oct 12, 2025

This makes \widehat work on Chrome.

@github-actions
Copy link

Wasm sizes:
Base branch: 111784 bytes
PR: 111808 bytes
Size diff: +24 bytes (0.02%)

@tmke8 tmke8 changed the title Use again a different Unicode symbol for \hat Use again a different Unicode symbol for \widehat Oct 12, 2025
@github-actions
Copy link

Wasm sizes:
Base branch: 111784 bytes
PR: 111808 bytes
Size diff: +24 bytes (0.02%)

@github-actions
Copy link

Wasm sizes:
Base branch: 111784 bytes
PR: 111808 bytes
Size diff: +24 bytes (0.02%)

@tmke8 tmke8 merged commit 33de387 into main Oct 12, 2025
13 checks passed
@tmke8 tmke8 deleted the new-hat branch October 12, 2025 19:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant